Nuprl Lemma : l_disjoint_intersection_implies
11,40
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
a
,
b
:(
T
List).
l_disjoint(
T
;
a
;l_intersection(
eq
;
a
;
b
))
l_disjoint(
T
;
a
;
b
)
latex
Definitions
x
:
A
.
B
(
x
)
,
(
x
l
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
Void
,
x
:
A
B
(
x
)
,
P
Q
,
False
,
A
,
type
List
,
EqDecider(
T
)
,
Type
,
P
Q
,
P
Q
,
x
.
t
(
x
)
,
{
T
}
,
l_disjoint(
T
;
l1
;
l2
)
Lemmas
implies
functionality
wrt
iff
,
all
functionality
wrt
iff
,
not
functionality
wrt
iff
,
and
functionality
wrt
iff
,
member-intersection
origin
T:Type, eq:EqDecider(T), a, b:(T List).
l_disjoint(T;a;b) T:Type, eq:EqDecider(T), a, b:(T List).
l_disjoint(T;a;b) x:A. B(x)
l)
B(x)
B(x) Q
A
Q Q
x. t(x)